Dafny Examples

Method: abs

method abs(x: int) returns (y: int)

ensures true

{

if x < 0 {

y := -x;

} else {

y := x;

}

}

1. method abs(x: int) returns (y: int):

• method: This keyword indicates the definition of a method. In Dafny, methods are used to define procedures that can take parameters, execute code, and return values.

• abs: The name of the method, which computes the absolute value of the input x.

• (x: int): A parameter x of type int (integer) that the method will accept.

• returns (y: int): Indicates that the method will return a value named y, which is also of type int.

2. ensures true:

• ensures: This keyword specifies a postcondition that must hold true when the method completes. Here, true indicates that there are no specific conditions that need to be met upon method completion.

3. if x < 0 {:

• This line starts a conditional statement that checks if x is less than 0.

4. y := -x;:

• y := -x;: This line assigns the negation of x to y if x is negative, effectively computing the absolute value.

5. else {:

• This marks the beginning of the alternative branch if x is not negative.

6. y := x;:

• If x is not negative, y is assigned the value of x, meaning the absolute value of a non-negative number is the number itself.

Method: foo

method foo(x: int)

requires x >= 0

{

var y := abs(x);

// assert( y == x);

}

1. method foo(x: int):

• Another method definition. This one is named foo and takes one parameter x of type int.

2. requires x >= 0:

• requires: This keyword introduces a precondition that must be satisfied before the method can be executed. In this case, x must be greater than or equal to 0.

3. var y := abs(x);:

• This line declares a variable y and assigns it the result of calling the abs method with x as the argument.

4. // assert( y == x);:

• This commented line suggests that there should be an assertion to check if y equals x. Since x is guaranteed to be non-negative, this assertion would hold true if the abs method is functioning correctly.

Method: max

method max(x: int, y: int) returns (m: int)

requires true;

ensures true;

{

var r : int;

if x > y {

r := 0;

} else {

r := 1;

}

m := r;

// return r;

// return m;

}

1. method max(x: int, y: int) returns (m: int):

• This defines a method named max that takes two integers x and y and returns an integer m.

2. requires true;:

• A precondition that is always satisfied (i.e., no restrictions on input values).

3. ensures true;:

• A postcondition that is always satisfied (no specific conditions required after execution).

4. var r : int;:

• Declares a variable r of type int.

5. if x > y {:

• Starts a conditional statement to check if x is greater than y.

6. r := 0;:

• If x is greater than y, assigns 0 to r.

7. else { r := 1; }:

• If x is not greater than y, assigns 1 to r.

8. m := r;:

• Assigns the value of r to the return variable m. Note: This is incorrect logic for finding the maximum; it should instead return x or y.

Method: ex1

method ex1(n: int)

requires true

ensures true

{

var i := 0;

while i < n

invariant true

// decreases *

{

i := i + 1;

}

// assert i == n;

}

1. method ex1(n: int):

• Defines a method named ex1 that takes an integer n.

2. requires true:

• No specific preconditions; the method can be called with any integer.

3. ensures true:

• No specific postconditions; the method will always complete successfully.

4. var i := 0;:

• Initializes a variable i to 0.

5. while i < n:

• Begins a while loop that continues as long as i is less than n.

6. invariant true:

• invariant: A condition that must hold true before and after each iteration of the loop. Here, it is always true, which means it doesn’t provide any useful information.

7. // decreases *:

• decreases: A clause that indicates a measure that decreases with each iteration of the loop, ensuring termination. In this case, it is left blank, which is incorrect for proving termination.

8. i := i + 1;:

• Increments i by 1 on each iteration.

9. // assert i == n;:

• A commented assertion to verify that after the loop, i should equal n.

Method: foo2

method foo2()

ensures false

decreases *

{

while true

decreases *

{

}

assert false;

}

1. method foo2():

• Defines a method foo2 that takes no parameters.

2. ensures false:

• Specifies a postcondition that can never be satisfied, indicating that this method will not terminate normally.

3. decreases *:

• Indicates an unspecified measure that is supposed to decrease, which does not apply because the method cannot complete normally.

4. while true:

• An infinite loop that will never terminate under normal circumstances.

5. assert false;:

• This assertion states that false should hold at this point, which is always incorrect, indicating that the method cannot reach this point without failing.

Method: find

method find(a: seq<int>, key: int) returns (index: int)

requires true

ensures true

{

index := 0;

while index < |a|

invariant true

{

if a[index] == key {

return 0;

}

index := index + 2;

}

index := -10;

}

1. method find(a: seq<int>, key: int) returns (index: int):

• Defines a method find that takes a sequence of integers a and an integer key, returning an integer index.

2. requires true:

• No preconditions for this method.

3. ensures true:

• No specific postconditions for this method.

4. index := 0;:

• Initializes the variable index to 0.

5. while index < |a|:

• Begins a while loop that continues as long as index is less than the length of sequence a.

6. invariant true:

• A loop invariant that is always true but does not provide meaningful information.

7. if a[index] == key { return 0; }:

• If the element at the current index in a equals key, the method returns 0, which is incorrect as it should return the index of the key.

8. index := index + 2;:

• Increments index by 2, skipping every other element.

9. index := -10;:

• After the loop ends, sets index to -10, which is not a meaningful result for the search.

Method: isPalindrome

method isPalindrome(a: seq<char>) returns (b

  

: bool)

{

return true;

}

1. method isPalindrome(a: seq<char>) returns (b: bool):

• Defines a method isPalindrome that takes a sequence of characters a and returns a boolean b.

2. return true;:

• The method currently always returns true, without any logic to check for a palindrome.

Predicate: sorted

predicate sorted(a: seq<int>)

{

forall j, k::0 <= j < k < |a| ==> a[j] <= a[k]

}

1. predicate sorted(a: seq<int>):

• Defines a predicate named sorted that checks if a sequence of integers a is sorted in ascending order.

2. forall j, k::0 <= j < k < |a| ==> a[j] <= a[k]:

• This quantifier states that for all indices j and k within the valid range of the sequence, if j is less than k, then the value at j must be less than or equal to the value at k.

Method: unique

method unique(a: seq<int>) returns (b: seq<int>)

requires sorted(a)

ensures true

{

return a;

}

1. method unique(a: seq<int>) returns (b: seq<int>):

• Defines a method unique that takes a sorted sequence of integers a and returns a sequence b.

2. requires sorted(a):

• Specifies a precondition that the input sequence must be sorted.

3. ensures true:

• No specific postconditions are required.

4. return a;:

• Currently, this method simply returns the input sequence a without removing duplicates.

Method: Main

method Main() {

var r := find([], 1);

print r, "\n";

  

r := find([0,3,5,7], 5);

print r, "\n";

  

var s1 := ['a'];

var r1 := isPalindrome(s1);

print "is [", s1, "]", " a isPalindrome? ", r1, " \n";

  

s1 := [];

r1 := isPalindrome(s1);

print "is [", s1, "]", " a isPalindrome? ", r1, " \n";

  

s1 := ['a', 'b'];

r1 := isPalindrome(s1);

print "is [", s1, "]", " a isPalindrome? ", r1, " \n";

  

s1 := ['a', 'b', 'a'];

r1 := isPalindrome(s1);

print "is [", s1, "]", " a isPalindrome? ", r1, " \n";

  

var i := [0,1,3,3,5,5,7];

var s := unique(i);

print "unique applied to ", i, " is ", s, "\n";

}

1. method Main() {:

• Defines the entry point for the program.

2. var r := find([], 1);:

• Calls the find method with an empty sequence and prints the result.

3. print r, "\n";:

• Prints the result of the find method followed by a newline.

4. Repeated Calls to isPalindrome:

• Several calls are made to the isPalindrome method with different character sequences, printing the results each time.

5. var i := [0,1,3,3,5,5,7];:

• Initializes a sequence of integers i with some duplicates.

6. var s := unique(i);:

• Calls the unique method to remove duplicates from the sequence.

7. print "unique applied to ", i, " is ", s, "\n";:

• Prints the result of applying the unique method to the sequence i.

Summary of Terms

• Method: A named sequence of instructions that can take inputs and return outputs.

• Ensures: Specifies the conditions that must hold true after the method execution.

• Requires: Specifies the conditions that must be true before executing the method.

• Invariant: A condition that holds true before and after each iteration of a loop.

• Decreases: A clause used to ensure that a loop will eventually terminate by indicating a measure that decreases with each iteration.

• Predicate: A function that returns a boolean value, typically used to specify properties of data.

• Return: The output of a method, indicated by the returns keyword.